(set-option :model_validate true)
(set-option :model.completion true)
(set-option :smt.arith.solver 5)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v5 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const Str0 String)
(declare-const Str1 String)
(declare-const Str10 String)
(declare-const Str17 String)
(assert (! v5 :named IP_1))
(assert (! (=> v2 v10) :named IP_2))
(assert (! v0 :named IP_3))
(assert (! (not v11) :named IP_4))
(check-sat)
(check-sat-assuming (IP_1 (not IP_3)))
(check-sat-assuming (IP_1 IP_4))
(check-sat-assuming (IP_3 IP_4))
(check-sat-assuming (IP_1 IP_2))
(check-sat-assuming (IP_2 IP_4))
(assert (! (not (str.contains Str10 Str17)) :named IP_5))
(push 1)
(check-sat)
(check-sat-assuming (IP_3 IP_5))
(check-sat-assuming (IP_1 IP_4))
(check-sat-assuming (IP_2 IP_5))
(check-sat-assuming (IP_1 IP_5))
(check-sat-assuming (IP_2 IP_4))